$\vdash$  $\forall$$P$:$\mathbb{P}$, $d$:Dec($P$), $T$:Type, $A$:($P$$\rightarrow$$T$), $B$:($\cap$$q$:$\neg$$P$.$T$). if $p$:$P$ then $A$($p$) else $B$ fi  $\in$ $T$